(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:
q0(0(x1)) → 0'(q1(x1))
q1(0(x1)) → 0(q1(x1))
q1(1'(x1)) → 1'(q1(x1))
0(q1(1(x1))) → q2(0(1'(x1)))
0'(q1(1(x1))) → q2(0'(1'(x1)))
1'(q1(1(x1))) → q2(1'(1'(x1)))
0(q2(0(x1))) → q2(0(0(x1)))
0'(q2(0(x1))) → q2(0'(0(x1)))
1'(q2(0(x1))) → q2(1'(0(x1)))
0(q2(1'(x1))) → q2(0(1'(x1)))
0'(q2(1'(x1))) → q2(0'(1'(x1)))
1'(q2(1'(x1))) → q2(1'(1'(x1)))
q2(0'(x1)) → 0'(q0(x1))
q0(1'(x1)) → 1'(q3(x1))
q3(1'(x1)) → 1'(q3(x1))
q3(b(x1)) → b(q4(x1))
Rewrite Strategy: INNERMOST
(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)
Converted CpxTRS to CDT
(2) Obligation:
Complexity Dependency Tuples Problem
Rules:
q0(0(z0)) → 0'(q1(z0))
q0(1'(z0)) → 1'(q3(z0))
q1(0(z0)) → 0(q1(z0))
q1(1'(z0)) → 1'(q1(z0))
0(q1(1(z0))) → q2(0(1'(z0)))
0(q2(0(z0))) → q2(0(0(z0)))
0(q2(1'(z0))) → q2(0(1'(z0)))
0'(q1(1(z0))) → q2(0'(1'(z0)))
0'(q2(0(z0))) → q2(0'(0(z0)))
0'(q2(1'(z0))) → q2(0'(1'(z0)))
1'(q1(1(z0))) → q2(1'(1'(z0)))
1'(q2(0(z0))) → q2(1'(0(z0)))
1'(q2(1'(z0))) → q2(1'(1'(z0)))
q2(0'(z0)) → 0'(q0(z0))
q3(1'(z0)) → 1'(q3(z0))
q3(b(z0)) → b(q4(z0))
Tuples:
Q0(0(z0)) → c(0''(q1(z0)), Q1(z0))
Q0(1'(z0)) → c1(1''(q3(z0)), Q3(z0))
Q1(0(z0)) → c2(01(q1(z0)), Q1(z0))
Q1(1'(z0)) → c3(1''(q1(z0)), Q1(z0))
01(q1(1(z0))) → c4(Q2(0(1'(z0))), 01(1'(z0)), 1''(z0))
01(q2(0(z0))) → c5(Q2(0(0(z0))), 01(0(z0)), 01(z0))
01(q2(1'(z0))) → c6(Q2(0(1'(z0))), 01(1'(z0)), 1''(z0))
0''(q1(1(z0))) → c7(Q2(0'(1'(z0))), 0''(1'(z0)), 1''(z0))
0''(q2(0(z0))) → c8(Q2(0'(0(z0))), 0''(0(z0)), 01(z0))
0''(q2(1'(z0))) → c9(Q2(0'(1'(z0))), 0''(1'(z0)), 1''(z0))
1''(q1(1(z0))) → c10(Q2(1'(1'(z0))), 1''(1'(z0)), 1''(z0))
1''(q2(0(z0))) → c11(Q2(1'(0(z0))), 1''(0(z0)), 01(z0))
1''(q2(1'(z0))) → c12(Q2(1'(1'(z0))), 1''(1'(z0)), 1''(z0))
Q2(0'(z0)) → c13(0''(q0(z0)), Q0(z0))
Q3(1'(z0)) → c14(1''(q3(z0)), Q3(z0))
S tuples:
Q0(0(z0)) → c(0''(q1(z0)), Q1(z0))
Q0(1'(z0)) → c1(1''(q3(z0)), Q3(z0))
Q1(0(z0)) → c2(01(q1(z0)), Q1(z0))
Q1(1'(z0)) → c3(1''(q1(z0)), Q1(z0))
01(q1(1(z0))) → c4(Q2(0(1'(z0))), 01(1'(z0)), 1''(z0))
01(q2(0(z0))) → c5(Q2(0(0(z0))), 01(0(z0)), 01(z0))
01(q2(1'(z0))) → c6(Q2(0(1'(z0))), 01(1'(z0)), 1''(z0))
0''(q1(1(z0))) → c7(Q2(0'(1'(z0))), 0''(1'(z0)), 1''(z0))
0''(q2(0(z0))) → c8(Q2(0'(0(z0))), 0''(0(z0)), 01(z0))
0''(q2(1'(z0))) → c9(Q2(0'(1'(z0))), 0''(1'(z0)), 1''(z0))
1''(q1(1(z0))) → c10(Q2(1'(1'(z0))), 1''(1'(z0)), 1''(z0))
1''(q2(0(z0))) → c11(Q2(1'(0(z0))), 1''(0(z0)), 01(z0))
1''(q2(1'(z0))) → c12(Q2(1'(1'(z0))), 1''(1'(z0)), 1''(z0))
Q2(0'(z0)) → c13(0''(q0(z0)), Q0(z0))
Q3(1'(z0)) → c14(1''(q3(z0)), Q3(z0))
K tuples:none
Defined Rule Symbols:
q0, q1, 0, 0', 1', q2, q3
Defined Pair Symbols:
Q0, Q1, 01, 0'', 1'', Q2, Q3
Compound Symbols:
c, c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14
(3) CdtUnreachableProof (EQUIVALENT transformation)
The following tuples could be removed as they are not reachable from basic start terms:
Q0(0(z0)) → c(0''(q1(z0)), Q1(z0))
Q0(1'(z0)) → c1(1''(q3(z0)), Q3(z0))
Q1(0(z0)) → c2(01(q1(z0)), Q1(z0))
Q1(1'(z0)) → c3(1''(q1(z0)), Q1(z0))
01(q1(1(z0))) → c4(Q2(0(1'(z0))), 01(1'(z0)), 1''(z0))
01(q2(0(z0))) → c5(Q2(0(0(z0))), 01(0(z0)), 01(z0))
01(q2(1'(z0))) → c6(Q2(0(1'(z0))), 01(1'(z0)), 1''(z0))
0''(q1(1(z0))) → c7(Q2(0'(1'(z0))), 0''(1'(z0)), 1''(z0))
0''(q2(0(z0))) → c8(Q2(0'(0(z0))), 0''(0(z0)), 01(z0))
0''(q2(1'(z0))) → c9(Q2(0'(1'(z0))), 0''(1'(z0)), 1''(z0))
1''(q1(1(z0))) → c10(Q2(1'(1'(z0))), 1''(1'(z0)), 1''(z0))
1''(q2(0(z0))) → c11(Q2(1'(0(z0))), 1''(0(z0)), 01(z0))
1''(q2(1'(z0))) → c12(Q2(1'(1'(z0))), 1''(1'(z0)), 1''(z0))
Q2(0'(z0)) → c13(0''(q0(z0)), Q0(z0))
Q3(1'(z0)) → c14(1''(q3(z0)), Q3(z0))
(4) Obligation:
Complexity Dependency Tuples Problem
Rules:
q0(0(z0)) → 0'(q1(z0))
q0(1'(z0)) → 1'(q3(z0))
q1(0(z0)) → 0(q1(z0))
q1(1'(z0)) → 1'(q1(z0))
0(q1(1(z0))) → q2(0(1'(z0)))
0(q2(0(z0))) → q2(0(0(z0)))
0(q2(1'(z0))) → q2(0(1'(z0)))
0'(q1(1(z0))) → q2(0'(1'(z0)))
0'(q2(0(z0))) → q2(0'(0(z0)))
0'(q2(1'(z0))) → q2(0'(1'(z0)))
1'(q1(1(z0))) → q2(1'(1'(z0)))
1'(q2(0(z0))) → q2(1'(0(z0)))
1'(q2(1'(z0))) → q2(1'(1'(z0)))
q2(0'(z0)) → 0'(q0(z0))
q3(1'(z0)) → 1'(q3(z0))
q3(b(z0)) → b(q4(z0))
Tuples:none
S tuples:none
K tuples:none
Defined Rule Symbols:
q0, q1, 0, 0', 1', q2, q3
Defined Pair Symbols:none
Compound Symbols:none
(5) SIsEmptyProof (EQUIVALENT transformation)
The set S is empty
(6) BOUNDS(O(1), O(1))